projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c3ca3d8) | patch
fixup for incremental solving
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 26 Nov 2012 17:40:31 +0000 (17:40 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 26 Nov 2012 17:40:31 +0000 (17:40 +0000)
commit78f459b303ed292a297a36cd0c435fdd025b0865
tree80be491bc4525d70d599fbd72869dd592f70d56atree
parentc3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0commit | diff
fixup for incremental solving
94 files changed:
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/minisat/core/Solver.cc diff | blob | history
src/prop/minisat/core/Solver.h diff | blob | history
src/prop/minisat/core/SolverTypes.h diff | blob | history
src/prop/minisat/minisat.cpp diff | blob | history
src/prop/minisat/minisat.h diff | blob | history
src/prop/minisat/simp/SimpSolver.cc diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/sat_solver.h diff | blob | history
src/prop/theory_proxy.cpp diff | blob | history
src/prop/theory_proxy.h diff | blob | history
src/theory/bv/bitblaster.cpp diff | blob | history
src/theory/logic_info.cpp diff | blob | history
src/theory/logic_info.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/arith/Makefile [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/Makefile [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_1.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_10.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_11.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_12.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_13.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_14.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_15.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_16.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_18.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_19.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_2.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_20.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_21.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_22.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_23.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_24.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_25.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_26.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_27.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_28.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_29.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_3.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_30.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_31.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_32.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_33.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_34.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_35.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_36.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_37.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_38.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_39.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_4.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_40.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_41.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_42.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_43.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_44.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_45.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_46.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_47.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_48.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_49.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_5.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_50.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_51.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_52.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_6.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_7.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_8.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/boolean/fuzz_9.smt2 [new file with mode: 0644] blob