We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Description: Z3 failed to runtests due to run test-z3.exe smt2print_parse under x86 mode. could you please look this issue? Thanks.
Reproduction steps:
Expected behavio: Runtests successfully.
Actual behavior: test.log test.log.62.log
spec: (declare-datatypes (T) ((list (nil) (cons (car T) (cdr list))))) (declare-const x Int) (declare-const l (list Int)) (declare-fun f ((list Int)) Bool) (assert (f (cons x l))) done parsing spec1: benchmark->string ; test (set-info :status unknown) (declare-datatypes ((list 1)) ((par (k!00)((nil) (cons (car k!00) (cdr (list k!00))))))) (declare-fun f ((list Int)) Bool) (declare-fun l () (list Int)) (declare-fun x () Int) (assert (let (($x8 (f (cons x l)))) (and $x8))) (check-sat)
attempting to parse spec1... parse successful, converting ast->string spec2: string->ast->string (ast-vector (and (f (cons x l)))) done printing spec: (declare-const x Int) (declare-const a (Array Int Int)) (declare-const b (Array (Array Int Int) Bool)) (assert (select b a)) (assert (= b ((as const (Array (Array Int Int) Bool)) true))) (assert (= b (store b a true))) (declare-const b1 (Array Bool Bool)) (declare-const b2 (Array Bool Bool)) (assert (= ((as const (Array Bool Bool)) false) ((_ map and) b1 b2))) ... ...
The text was updated successfully, but these errors were encountered:
d289434
fix Z3Prover#6535
effc343
No branches or pull requests
Description:
Z3 failed to runtests due to run test-z3.exe smt2print_parse under x86 mode. could you please look this issue? Thanks.
Reproduction steps:
Expected behavio:
Runtests successfully.
Actual behavior:
test.log
test.log.62.log
spec:
(declare-datatypes (T) ((list (nil) (cons (car T) (cdr list)))))
(declare-const x Int)
(declare-const l (list Int))
(declare-fun f ((list Int)) Bool)
(assert (f (cons x l)))
done parsing
spec1: benchmark->string
; test
(set-info :status unknown)
(declare-datatypes ((list 1)) ((par (k!00)((nil) (cons (car k!00) (cdr (list k!00)))))))
(declare-fun f ((list Int)) Bool)
(declare-fun l () (list Int))
(declare-fun x () Int)
(assert
(let (($x8 (f (cons x l))))
(and $x8)))
(check-sat)
attempting to parse spec1...
parse successful, converting ast->string
spec2: string->ast->string
(ast-vector
(and (f (cons x l))))
done printing
spec:
(declare-const x Int)
(declare-const a (Array Int Int))
(declare-const b (Array (Array Int Int) Bool))
(assert (select b a))
(assert (= b ((as const (Array (Array Int Int) Bool)) true)))
(assert (= b (store b a true)))
(declare-const b1 (Array Bool Bool))
(declare-const b2 (Array Bool Bool))
(assert (= ((as const (Array Bool Bool)) false) ((_ map and) b1 b2)))
... ...
The text was updated successfully, but these errors were encountered: